| Definitions | t  T, FinProbSpace, *50/50*, P & Q,  a  j < b. E(j), ||as||, l[i],  xL. P(x), r s, (r/s), x:A. B(x), P   Q,  A, P  Q,  b, qeq(r;s), P Q,  , if b then t else f fi , tt, (i = j), ff, True, False, A c B,   x. t(x), A B, (r) i k < j. E(k),  lb i < ub. E(i), (op,id) lb i < ub. E(i), Y, i <z j, x f y, *, t.1, t.2, r +gp, +r, < +*>, r + s, e, 0, hd(l), nth_tl(n;as), i z j,  b, r * s, 1/r, tl(l), SQType(T), {T}, a b, , <+>, q_le(r;s), p  q, qpositive(r), r - s, p q, {i..j }, x(s), i j < k, (x l),  x:A. B(x),  , Dec(P), P Q, S  T |